i, a, x:Id, X, T:Type, x0:X, P:(XTProp).
Normal(T)  Normal(X)  (x:X. Dec(v:T. P(x,v)))  R-Feasible(R-pre-init1(i;x;X;x0;a;T;P)) 

latex

Definitions

b, t  T, Id, Type, x.A(x), x:A. B(x), x. t(x), x : v, State(ds), f(a), x:AB(x), x:A. B(x), Dec(P), Normal(ds), Void, f(x)?z, a:A fp B(a), P  Q, x:AB(x), {x:A| B(x) }, Top, x:A. B(x), IdDeq, P  Q, R-pre-init1(i;x;A;x0;a;T;P), Prop, Normal(T), R-Feasible(R), if b t else f fi, false, eqof(d), p  q, f(x), x  dom(f), P & Q, True, true, A, b, p  q, , s = t, False, left+right, P  Q, P  Q, T, Unit, x,y. t(x;y)

Lemmas

fpf-all-single, iff wf, fpf-dom wf, fpf-trivial-subtype-top, eqtt to assert, assert of bor, eqff to assert, squash wf, bnot thru bor, iff transitivity, assert of band, and functionality wrt iff, assert of bnot, false wf, bool wf, band wf, bnot wf, not wf, assert wf, btrue wf, true wf, ifthenelse wf, bor wf, eqof wf, bfalse wf, eq id self, subtype rel self, decidable wf, normal-type wf, R-pre-init-feasible, fpf-cap-single1, id-deq wf, top wf, decl-state wf, fpf-single wf, Id wf